/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
/**
 * NuGat-API named Chameleon developed by Simon De Baets to Verimag.
 *
 */
package chameleon.model.NuGatManager.Strategy;

import chameleon.model.NuGatStructure.game.GamePlayer;
import chameleon.model.NuGatStructure.prop.PropGame;
import chameleon.model.NuGatStructure.opt.OptGame;
import chameleon.model.NuGatStructure.utils.Node;
import chameleon.model.NuGatStructure.fsm.GameBddFsm;
import chameleon.model.NuGatStructure.bdd.Bdd;
import chameleon.model.NuGatStructure.bdd.DdManager;
import chameleon.model.NuGatStructure.enc.BddEnc;
import chameleon.model.NuGatStructure.strategy.GameStrategy;
import chameleon.gameSolver.NuGat.NuGatInterface;
import chameleon.model.NuGatStructure.strategy.AvoidDeadlockStrategy;
import chameleon.model.NuGatStructure.strategy.AvoidTargetStrategy;
import chameleon.model.NuGatStructure.strategy.ReachAvoidStrategy;
import chameleon.model.NuGatStructure.strategy.ReachDeadlockStrategy;
import chameleon.model.NuGatStructure.strategy.ReachTargetStrategy;
import chameleon.model.game.Game;
import com.sun.jna.Pointer;

/**
 * This class compute a strategy to a safety game (REACHTARGET, REACHDEADLOCK,
 * AVOIDTARGET, AVOIDDEADLOCK).
 * @author simon
 */
public class SafetyStrategyComputation {
    
    private NuGatInterface nugat_;
    private PreImage preImage_;
    private Game game_;
    
    public SafetyStrategyComputation(NuGatInterface nugat, PreImage preImage, Game game){
        nugat_ = nugat;
        preImage_ = preImage;
        game_ = game;
    }
    
    
    public GameStrategy computeStrategy(){
        /*This method provide from NuGat gameCheckReachAvoidSpec.c:: 
        Game_UseStrongReachabilityAlgorithm*/
        
        /*-----------------------------------------------------------------------*/
        /*-------------         STRATEGY COMPUTATION        ---------------------*/
        /*-----------------------------------------------------------------------*/
        /* strategy is computed only if the container for the strategy is provided.
         The strategy is computed for the player if the game is won and for the
         opponent if the game is lost.

        */
        
        //Initialisation of paramter (compute in PremImageComputation)
        
        GameStrategy strategy = null;
        
        Node constructNode = new Node (Pointer.NULL,nugat_);
        Node reachStateList = preImage_.getReachStateList();
        GamePlayer player = preImage_.getPlayer();
        GamePlayer opponent = preImage_.getOpponent();
        char quantifiers = preImage_.getQuantifiers();
        Bdd allReachStates = preImage_.getAllReachStates();
        Bdd originalTarget = preImage_.getOriginalTarget();
        boolean isFixedpointReached = preImage_.isFixedpointReached();
        boolean isTargetReached = preImage_.isTargetReached();
        GameBddFsm fsm = game_.getGameBddFsm();
        GamePlayer PLAYER_1 = new GamePlayer(nugat_.PLAYER_NAME_1,nugat_);
        GamePlayer PLAYER_2 = new GamePlayer(nugat_.PLAYER_NAME_2,nugat_);
        OptGame oh = game_.getOptsHandlerInstance();
        
        
        BddEnc enc = game_.getBddEncoding();
        DdManager dd_manager = enc.getDdManager();
        
        Bdd trans = dd_manager.bddZero();

        /* Compute the transitions for the strategy */

        /* The target is reached =>
           the player won in a reachability game or lost in an avoidance game
        */
        if (isTargetReached) {
            Node iter;
            Node targ, diff;
            Node diffReachStateList;

            /* At first, create a list of differences between consecutive
             reach states.
             NB: reachStateList list is decreasing, i.e. first step is at
             the beginning, the original target is at the end.
            */
            
            
            for (iter = reachStateList, diffReachStateList = new Node (Pointer.NULL, nugat_);
                iter.notNull() && (iter.cdr()).notNull();
                iter = iter.cdr()) {
                Bdd not_prev = dd_manager.bddNot(new Bdd((iter.cdr()).car(),nugat_));
                Bdd and = dd_manager.bddAnd(new Bdd(iter.car(),nugat_), not_prev);
                dd_manager.bddFree(not_prev);
                diffReachStateList = constructNode.cons(new Node (and.ptr(),nugat_),
                        diffReachStateList);
            }
            diffReachStateList = diffReachStateList.reverse();

            /* Compute moves (transitions). They should include also opponent-deadlock
             moves
            */
          
            targ = reachStateList.cdr();
            diff = diffReachStateList;
      
            while (targ.notNull()) {
                Bdd move;
                /* move =
                   for player 1 :
                   diff & trans1 & next(invar1) &
                   Any p2', trans2 & next(invar2) -> next(targ)
                   for player 2 :
                   diff & trans1 & next(invar1) &
                   trans2 & next(invar2) & next(targ)

                   Actually, for the first player opponent-deadlock moves are
                   removed by getMove.  They will be added later
                   in a separate field.
                */
                move = fsm.getMove(new Bdd(targ.car(),nugat_), player);
                move = dd_manager.bddAndAccumulate( move, new Bdd (diff.car(),nugat_));

                trans = dd_manager.bddOrAccumulate(trans, move);

                dd_manager.bddFree(move);
                targ = targ.cdr();
                diff = diff.cdr();
                assert((!targ.notNull()) == (!diff.notNull()));
            } /* while */

            /* add back the opponent-deadlock moves for the first player */
            if (PLAYER_1.equals(player)) {
                trans = dd_manager.bddOrAccumulate(trans,
                              fsm.gameBddFsmWithoutSuccessorStates(PLAYER_2));
            }

            /* free the list of reach-states differences, i.e. diffReachStateList */
            while (diffReachStateList.notNull()) {
                Node n = diffReachStateList.cdr();
                dd_manager.bddFree(new Bdd(diffReachStateList.car(),nugat_));
                diffReachStateList.freeNode();
                diffReachStateList = n;
            }
            /* initial quantifiers have been
                                  reversed => reverse */
            int param;
            if(quantifiers !=
                oh.gameInitialCondition())
                param = 1;
            else
                param = 0;
                                  
            
            /* construct the strategy */
            strategy = constructStrategy(fsm,
                              player,
                              param,
                              originalTarget,
                              allReachStates,
                              trans);

        } /* end of if (isTargetReached) */

        /* fixed point is reached =>
           the player lost in a reachability game or won in an avoidance game
        */
        else if (isFixedpointReached) {
              Bdd winStates, zero;

              /* for the player (opponent) it is just necessary to stay in the
                 not-reach states */
              winStates = dd_manager.bddNot(allReachStates);

              trans = fsm.getMove(winStates, opponent);
              trans = dd_manager.bddAndAccumulate(trans, winStates);


              /* for player 1 getMove removes opponent deadlock states.
                 Add them back now.
              */
              if (PLAYER_1.equals(opponent)) {
                trans = dd_manager.bddOrAccumulate(trans,
                                  fsm.gameBddFsmWithoutSuccessorStates(PLAYER_2));
              }

              zero = dd_manager.bddZero();
              
              int param;
                if(quantifiers !=
                    oh.gameInitialCondition())
                    param = 1;
                else
                    param = 0;

              /* construct the strategy */
              strategy =
                        constructStrategy(fsm,
                                       opponent,
                                       param,
                                       zero,
                                       winStates,
                                       trans);

              dd_manager.bddFree(zero);
              dd_manager.bddFree(winStates);
        } /* end of else if (isFixedpointReached)*/

        else {
          /* if the target is not reached then the fixpoint is reached always */
         assert(false);
        }

        /* end of reach- or avoid- strategy computation */


        /*-----    FREE THE CREATED OBJECTS    --------------------------------------*/

        /* free reachStateList */
        while (reachStateList.notNull()) {
            Node n = reachStateList.cdr();
            dd_manager.bddFree(new Bdd(reachStateList.car(),nugat_));
            reachStateList.freeNode();
            reachStateList = n;
        }
        
        dd_manager.bddFree(allReachStates);
        dd_manager.bddFree(originalTarget);
        
        
        
        return strategy;
    }
    
    private ReachAvoidStrategy constructStrategy (GameBddFsm fsm,
                                                    GamePlayer player,
                                                    int param,
                                                    Bdd originalTarget,
                                                    Bdd allReachStates,
                                                    Bdd trans){
        PropGame prop = preImage_.getProp();
        int type = prop.getType();
        
        if (type == nugat_.PropGame_AvoidDeadlock){
            return new AvoidDeadlockStrategy(fsm,
                              player,
                              param,
                              originalTarget,
                              allReachStates,
                              trans,
                              preImage_,
                              prop,
                              nugat_);
        }
        else if (type == nugat_.PropGame_AvoidTarget){
            return new AvoidTargetStrategy(fsm,
                              player,
                              param,
                              originalTarget,
                              allReachStates,
                              trans,
                              preImage_,
                              prop,
                              nugat_);
        }
        else if (type == nugat_.PropGame_ReachTarget){
            return new ReachTargetStrategy(fsm,
                              player,
                              param,
                              originalTarget,
                              allReachStates,
                              trans,
                              preImage_,
                              prop,
                              nugat_);
        }
        else if (type == nugat_.PropGame_ReachDeadlock){
            return new ReachDeadlockStrategy(fsm,
                              player,
                              param,
                              originalTarget,
                              allReachStates,
                              trans,
                              preImage_,
                              prop,
                              nugat_);
        }
        else{
            throw new RuntimeException("Try to build a reach avoid strategy with a wrong type of game");
        }
        
    }
}
